Section: New Results

Verification of Security Protocols in the Symbolic Model

Participants : Bruno Blanchet, Marc Sylvestre.

The applied pi calculus is a widely used language for modeling security protocols, including as a theoretical basis of ProVerif . However, the seminal paper that describes this language  [45] does not come with proofs, and detailed proofs for the results in this paper were never published. Martín Abadi, Bruno Blanchet, and Cédric Fournet wrote detailed proofs of all results of this paper. This work appears in the Journal of the ACM [12].

Marc Sylvestre improved the display of attacks in ProVerif, in particular by showing the computations performed by the attacker to obtain the messages sent in the attack, and by explaining why the found trace breaks the considered security property. He also developed an interactive simulator that allows the user to run the protocol step by step. The extended tool is available at http://proverif.inria.fr.